\documentclass[a4paper,10pt,oneside,reqno]{article}

\usepackage{amsfonts, amsmath, amsthm, amssymb}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage[all,cmtip]{xy}
\usepackage{graphicx}
\usepackage{lmodern}
\usepackage{microtype}
\usepackage[utf8]{inputenc}
\usepackage{booktabs}
\usepackage{a4wide}
\usepackage{comment}
\usepackage{array}
\usepackage[colorlinks=true,linkcolor=blue,urlcolor=blue]{hyperref}
\usepackage[lofdepth,lotdepth]{subfig}
\usepackage{tikz}
\usetikzlibrary{decorations.pathreplacing,patterns}
\pagestyle{plain}

\usepackage{array}

%\hypersetup{
%    pdfborder = {0 0 0}
%}

\DeclareMathOperator{\tr}{tr}

\newcommand{\mint}[1]{\text{#1}}
\newcommand{\then}{\Rightarrow}
\newcommand{\Then}{\Longrightarrow}
\newcommand{\trans}{\rightsquigarrow}
\newcommand{\tend}{t_{\text{end}}}

%\newcommand{\vec}[1]{\mathbf{#1}}
\newcommand{\w}{\mathbf{v}}
\renewcommand{\c}{\mathbf{c}}

\newtheorem*{quest}{Task}
\newtheorem{thm}{Theorem}
\newtheorem{lemma}{Lemma}

%\renewcommand{\thesubsection}{\thesection.\alph{subsection}}

%\frenchspacing

\hypersetup{pdftitle={Reasoning w/CS: SMT; Tejiscak}}
\title{Reasoning with Computer support: SMT}
\author{Matúš Tejiščák (\url{ziman@functor.sk})\\ 4176200}
\date{\today}
\begin{document}

\maketitle

\section{Job scheduling}

\subsection{Representation}

We represent the solution as a vector $\{s_i\}_{i=1}^{12}$, where $s_i$ denotes the
\emph{starting time} of the job number $i$. Time blocks are numbered starting from zero.

We also introduce a constant $\tend$ equal to the number of the first time block when
all jobs must be finished. Obviously, the schedule is trivial (serial) for $\tend = 1 + \ldots + 12$.
By bisection, we will try to find the least $\tend$ that allows for satisfiability of the problem.

\subsection{Constraints}

First, we list the big-picture constraints:
\begin{itemize}
	\item All jobs must fit between $0$ and $\tend$:
	\begin{equation}
		\bigwedge_{i=1}^{12} (0 \leq s_i) \wedge (s_i + i < \tend)
	\end{equation}
	
	\item Dependencies between jobs must be satisfied:
	\begin{equation}
		\mathsf{deps}(\{
			\{1,2\} \trans 3,
			\{3,4\} \trans 5,
			\{3,4,6\} \trans 7,
			\{5,8\} \trans 9,
			\{10\} \trans 11,
			\{9,11\} \trans 12
		\})
	\end{equation}

	\item No more than two \emph{critical jobs} simultaneously:
	\begin{equation}
		\bigwedge_{t=0}^{\tend-1} \mathsf{critJobs}(t) \leq 2
	\end{equation}
\end{itemize}
Now let's make it precise what \textsf{deps} and \textsf{critJobs} exactly mean. The \textsf{deps}
predicate states that a job cannot be started before its prerequisites are done:
\begin{equation}
	\mathsf{deps}(X) = \bigwedge_{P \trans j \in X} \bigwedge_{p \in P} s_p + p \leq s_j
\end{equation}
We also want to count the number of simultaneous \emph{critical jobs} that are using the limited
equipment at the time $t$:
\begin{equation}
	\mathsf{critJobs}(t) = \sum_{j = 4}^{10}
		\mathsf{if} \; (t \geq s_j) \wedge (t < s_j + j) \; \mathsf{then} \; 1 \; \mathsf{else} \; 0
\end{equation}

\subsection{Implementation}

Implementation was done using a \textsf{Haskell} EDSL generating \textsf{Yices} code.\footnote{
	\url{http://code.google.com/p/reasoning-homework/source/browse/trunk/rcs-task1.hs}
}

\subsection{Solution}

By the means of binary search, starting from $1 + \ldots + 12 = 78$, we can observe that the lowest
satisfiable value of $\tend$ is $36$. Then a consultation with \textsf{Yices} looks as follows:
\begin{verbatim}
ziman@idefix:~/dev/reasoning $ runhaskell rcs-task1.hs | yices -e -tc
sat
(= (s 1) 0)
(= (s 2) 0)
(= (s 3) 2)
(= (s 4) 3)
(= (s 5) 10)
(= (s 6) 18)
(= (s 7) 29)
(= (s 8) 7)
(= (s 9) 15)
(= (s 10) 0)
(= (s 11) 10)
(= (s 12) 24)
\end{verbatim}
Hence the total running time is $36$ units of time, with the following schedule
(Figure \ref{fig:optimal-schedule}).

\begin{figure}[htp]
	\centering
	\begin{tikzpicture}[x=3.5mm,y=5mm]
		\draw[step=1,gray,dotted] (0,0) grid (36,12);
		\draw[dotted,thick] (10,0) -- (10,12);
		\draw[dotted,thick] (20,0) -- (20,12);
		\draw[dotted,thick] (30,0) -- (30,12);
		\begin{scope}[ultra thick,fill=white]
			\filldraw (0,0) rectangle +(1,1);
			\filldraw (0,1) rectangle +(2,1);
			\filldraw (2,2) rectangle +(3,1);
			\begin{scope}[pattern=crosshatch dots]
				\filldraw (3,3) rectangle +(4,1);
				\filldraw (10,4) rectangle +(5,1);
				\filldraw (18,5) rectangle +(6,1);
				\filldraw (29,6) rectangle +(7,1);
				\filldraw (7,7) rectangle +(8,1);
				\filldraw (15,8) rectangle +(9,1);
				\filldraw (0,9) rectangle +(10,1);
			\end{scope}
			\filldraw (10,10) rectangle +(11,1);
			\filldraw (24,11) rectangle +(12,1);
		\end{scope}
		\foreach \i in {1,...,12} {
			\draw (0,\i-0.5) node[left]{\i};
		}
	\end{tikzpicture}
	\caption{An optimal schedule found by \textsf{Yices}; \emph{critical jobs}
		are filled with dots.}
	\label{fig:optimal-schedule}
\end{figure}


\section{Truck loading}
\subsection{Representation}

Having $G$ goods and $N$ trucks, we can represent any solution as an $N \times G$ matrix $L$,
symbolizing that the truck $n$ carries $L_{ng}$ pallets of the goods $g$.
\begin{equation}
	L = \left(
	\begin{matrix}
		L_{11} & L_{12} & L_{13} & \cdots & L_{1G} \\
		L_{21} & L_{22} & L_{23} & \cdots & L_{2G} \\
		L_{31} & L_{32} & L_{33} & \cdots & L_{3G} \\
		       & \vdots &        & \ddots & \vdots \\
		L_{N1} & L_{N2} & L_{N3} & \cdots & L_{NG}
	\end{matrix} \right)
\end{equation}

We represent the weight of each goods as a column vector $\w$ of type $G \times 1$ and
the required count of pallets for each goods as a vector $\c$, also of type $G \times 1$.
\begin{equation}
	\w = \left(
	\begin{matrix}
		w_1 \\ w_2 \\ w_3 \\ \vdots \\ w_G
	\end{matrix} \right); \quad
	\c = \left(
	\begin{matrix}
		c_1 \\ c_2 \\ c_3 \\ \vdots \\ c_G
	\end{matrix} \right)
\end{equation}

\subsection{Constraints}
Let us also use the name $w_{\max}$ for the maximum load of each truck and $c_{\max}$
for the maximum count of pallets for each truck. Then we have the following constraints:
\begin{align}
	L_{ng} &\geq 0
		& \text{(consistency of load)} \\
	L^T \cdot [1]_{N \times 1} &= \c
		& \text{(required count of pallets per each goods)} \\
	L \cdot [1]_{G \times 1} &\leq [c_{\max}]_{N \times 1}
		& \text{(space constraints for each truck)} \\
	L \cdot \w &\leq [w_{\max}]_{N \times 1}
		& \text{(weight constraints for each truck)}
\end{align}

This is all it takes to encode this problem. The length of the encoding is obviously
$O(NG)$, since we have three vector (in)equations, each dealing with a single matrix-time-vector
expression that is compared to another vector (the first inequality is obviously $O(NG)$).

\subsection{Implementation}

We solved this task using \textsf{Yices}, encoding the problem in a \textsf{Haskell} EDSL
designed for this purpose. In the \textsf{Haskell} program\footnote{
\url{http://code.google.com/p/reasoning-homework/source/browse/trunk/Task1.hs}
}, we defined functions with rather
intuitive names instead of using direct matrix operations (although the functions essentially
don't encode anything more than matrix operations).

The \textsf{Haskell} EDSL gives us the convenience of expressing the formulas in a compact way
(using recursion, quantifiers, abstraction etc.), while it automatically expands the formulas
into first-order terms behind the scenes.

We also used a custom data type for the goods. Thus, we do not represent the goods using numbers
but using a specialized data type for readability.

Finding the maximum count of beer pallets was done by varying the beer-related component
of the vector $\c$ and seeing whether the resulting formula is still satisfiable.

\subsection{Solution}

We discovered that the maximum number of beer pallets that can be loaded is 19. A possible
load distribution in that case is given below.

\begin{table}[htp]
	\centering{
	\begin{tabular}{cccccc}
		truck & cheese & beer & wine & drinks & chips \\
		1& 2&2&3&1&0 \\
		2& 1&6&0&0&0 \\
		3& 0&3&3&1&1 \\
		4& 0&1&1&4&2 \\
		5& 0&3&0&3&1 \\
		6& 1&4&1&1&1 \\
		\hline
		&4&19&8&10&5\\
	\end{tabular}
	}
	\caption{An optimal solution: we can load 19 pallets of beer.}
\end{table}

\section{School schedule}

\subsection{Representation}

The solution is represented as a vector
$\{s_i\}_{i=1}^{10} \in \{\mathsf{first}, \mathsf{second}, \mathsf{none}\}^{10}$ of scheduling
assignments, where $s_i$ denotes when the course $A_i$ is scheduled: either in the first semester,
second semester or not at all.

We also have a function $\mathsf{ects}(c)$ that, given the number of the course, returns the number
of ECTS assigned to that course.

\subsection{Constraints}

In both semesters exactly 30 ECTS have to be followed and in the second semester, a 20-ECTS final
project has to be done. That simply means we need to schedule 30 ECTS in the first semester
and 10 ECTS in the second semester.

Again, we list the big-picture constraints first.
\begin{itemize}
	\item The ,,at least two'' constraints:
	\begin{equation}
		\mathsf{atLeastTwoOf}(\{1,\ldots, 4\})
		\wedge \mathsf{atLeastTwoOf}(\{5,\ldots, 7\})
		\wedge \mathsf{atLeastTwoOf}(\{8,\ldots, 10\})
	\end{equation}
	
	\item Prerequisites:
	\begin{equation}
		\mathsf{prereq}(8,1) \wedge \mathsf{prereq}(9,2) \wedge \mathsf{prereq}(9,3)
	\end{equation}
	
	\item Incompatibilities:
	\begin{equation}
		\mathsf{incompat}(7,10)
	\end{equation}
	
	\item Total ECTS counts:
	\begin{equation}
		[\mathsf{semesterECTS}(\mathsf{first}) = 30]
		\wedge [\mathsf{semesterECTS}(\mathsf{second}) = 10]
	\end{equation}
\end{itemize}

Now we list all the auxiliary predicates used. These definitions could be unfolded directly
in the big formula but this way it is much more readable -- and in the \textsf{Haskell} code, we use
these predicates in this form as well.

We enforce the ,,at least two'' constraint by building a formula over all pairs of courses
in the given set:
\begin{equation}
	\mathsf{atLeastTwoOf}(X) = \bigvee_{i < j \in X}
		(s_i \neq \mathsf{none}) \wedge (s_j \neq \mathsf{none})
\end{equation}

Enforcing prerequisites is done as follows: either the depending course is not followed at all
or it must be the case that the depending course is followed in the second semester \emph{and}
the dependency is followed in the first semester.
\begin{equation}
	\mathsf{prereq}(c,d) = (s_c = \mathsf{none})
		\vee \big[(s_c = \mathsf{second}) \wedge (s_d = \mathsf{first})\big]	
\end{equation}

Incompatibility is easy: out of two incompatible courses, at least one must not be followed.
\begin{equation}
	\mathsf{incompat}(c,d) = (s_c = \mathsf{none}) \vee (s_d = \mathsf{none})
\end{equation}

What's left is to define the total ECTS count of courses followed in either semester.
\begin{equation}
	\mathsf{semesterECTS}(s) = \sum_{c = 1}^{10}
		\mathsf{if} \; s_c \neq \mathsf{none} \;
			\mathsf{then} \; \mathsf{ects}(s) \; \mathsf{else} \; 0
\end{equation}

\subsection{Implementation}

Implementation was done using a \textsf{Haskell} EDSL generating \textsf{Yices} code.\footnote{
	\url{http://code.google.com/p/reasoning-homework/source/browse/trunk/rcs-task3.hs}
}

\subsection{Solution}

By running the \textsf{Yices} program, we obtain the validation listed in the following
consultation.

\begin{verbatim}
ziman@idefix:~/dev/reasoning $ runhaskell rcs-task3.hs | yices -tc -e
sat
(= (s 1) second)
(= (s 2) first)
(= (s 3) first)
(= (s 4) first)
(= (s 5) first)
(= (s 6) first)
(= (s 7) none)
(= (s 8) none)
(= (s 9) second)
(= (s 10) first)
\end{verbatim}
This solution is visualized in Table \ref{tab:semesters}, along with the coresponding ECTS
counts and total sums.

\begin{table}[htp]
	\centering
	\begin{tabular}{crcr} \toprule
		\multicolumn{2}{c}{\textit{First semester}}
			& \multicolumn{2}{c}{\textit{Second semester}} \\
		\cmidrule(r){1-2} \cmidrule(r){3-4}
		Course & ECTS & Course & ECTS \\
		\midrule
		$A_2$ & 5 & $A_1$ & 4 \\
		$A_3$ & 4 & $A_9$ & 6 \\
		$A_4$ & 5 & Project & 20 \\
		$A_5$ & 4 &  &  \\
		$A_6$ & 6 &  &  \\
		$A_{10}$ & 6 &  &  \\
		\midrule
		Total: & 30 & & 30 \\
		\bottomrule		
	\end{tabular}
	\caption{Courses followed in different semesters.}
	\label{tab:semesters}
\end{table}



\end{document}






























































